COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notions of finite union and finite sum
C00003 00003	(proof sums)
C00005 00004	(proof sumfacts)
C00006 00005	proof of properties of union and sum
C00009 ENDMK
C⊗;
;the notions of finite union and finite sum
(wipe-out)
(get-proof set)
(get-proofs minus)

(proof sums)

(decl totalfunction (type: |(ground→ground)→truthval|))
(define totalfunction |∀f.totalfunction(f)≡(∀n.natnum f(n))|)
(label tot_funct)

(decl numseq (type:|ground→ground|)(sort: totalfunction))
(decl sum (type: |(@numseq)⊗(@n)→(@n)|) (syntype: constant))
(decl setseq (type: |@n→@set|))
(decl un (type: |(@setseq)⊗(@n)→(@set)|) (syntype: constant))

;axiom for sum
(defax sum |∀n numseq.sum(numseq,0)=0∧sum(numseq,n')=sum(numseq,n)+numseq(n)|)
(label sumdef)

(defax un |∀n setseq.un(setseq,0)=emptyset∧un(setseq,n')=un(setseq,n)∪setseq(n)|)
(label undef)

(decl disj_pair (type: |(@set⊗@set)→truthval|))
(define disj_pair |∀a b.disj_pair(a,b)=emptyp(a∩b)|)
(label dijpair_def)

(decl disjoint (type: |((ground→@set)⊗ground)→truthval|))
(defax disjoint |∀n setseq.disjoint(setseq,0)∧
    disjoint(setseq,n')=(disjoint(setseq,n)∧disj_pair(un(setseq,n),setseq(n)))| )
(label disjointdef)
(proof sumfacts)

;properties of un

(axiom |∀setseq n m.m<n⊃setseq(m)⊂un(setseq,n)|)
(label unionfact1)

;exercise: unionfact2 
;∀setseq n m.n<m⊃un(setseq,n)⊂un(setseq,m)

;properties of sum

(axiom |∀k numseq.natnum(numseq(k))|) 
(label simpinfo)(label numseq_total)

(axiom |∀k numseq.natnum(sum(numseq,k))|)
(label simpinfo)(label sumsort)
(save-proofs sums)
;proof of properties of union and sum
(wipe-out)
(get-proofs sums)
(proof unionfacts)

;properties of union

;unionfact1

(ue (a |λn.m<n⊃(∀xv.(setseq(m))(xv)⊃(un(setseq,n))(xv))|) proof_by_induction
   (open un union) 
    (use less_succ_lesseq mode: always) (open lesseq) (use normal mode: always))
;∀N.M<N⊃(∀XV.(SETSEQ(M))(XV)⊃(UN(SETSEQ,N))(XV))

;properties of sum

;numseq_total

(trw |∀numseq.totalfunction(numseq)|)
;∀NUMSEQ.TOTALFUNCTION(NUMSEQ)

(unlabel simpinfo numseq_total)
(rw * (open totalfunction))
;∀NUMSEQ N.NATNUM(NUMSEQ(N))
(label simpinfo numseq_total)

;sumsort

(unlabel simpinfo sumsort)
(ue (a |λn.natnum(sum(numseq,n))|) proof_by_induction (open sum))
;∀N.NATNUM(SUM(NUMSEQ,N))
(label simpinfo sumsort)